k:Knd. isrcv(k)  k = rcv(lnk(k),tag(k)) 

latex

Definitions	t  T, x:A. B(x), rcv(l,tg), False, True, P  Q, b, Knd, tag(k), lnk(k), isrcv(k)
Lemmas	assert wf, isrcv wf, Knd wf, true wf, false wf, rcv wf